nLab cartesian closed category

Definition

A cartesian closed category (sometimes: ccc) is a category with finite products which is closed with respect to its cartesian monoidal structure.

The internal hom $[S,X]$ in a cartesian closed category is often called exponentiation and is denoted $X^S$.

A cartesian closed functor between cartesian closed categories $C$, $D$ is a functor $F \colon C \to D$ that is product-preserving and that is also exponential-preserving, meaning that the canonical map

$$F(a^b) \to F(a)^{F(b)},$$

corresponding to the composite

$$F(a^b) \times F(b) \cong F(a^b \times b) \stackrel{F(eval_{a, b})}{\to} F(a),$$

is an isomorphism.

Examples

• Any topos or quasitopos, such as Set, is cartesian closed.

  See also closed monoidal structure on presheaves.

• Cat is also cartesian closed. (Cf. e.g. p. 98 of Mac Lane, 2nd ed., or the remark below Definition 4.3.9 in Riehl.)

• Many nice categories of topological spaces are also cartesian closed, particularly the convenient categories of spaces.

Some basic consequences

A category is cartesian closed if it has finite products and if for any two objects $X$, $Y$, there is an object $Y^X$ (thought of as a “space of maps from $X$ to $Y$”) such that for any object $Z$, there is a bijection between the set of maps $Z \to Y^X$ and the set of maps $Z \times X \to Y$, and this bijection is natural in $Z$.

There is an evaluation map $ev_{X, Y}: Y^X \times X \to Y$, which by definition is the map corresponding to the identity map $Y^X \to Y^X$ under the bijection. Using the naturality, it may be shown that the bijection $\hom(Z, Y^X) \to \hom(Z \times X, Y)$ takes a map $\phi: Z \to Y^X$ to the composite

$$Z \times X \stackrel{\phi \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y$$

and the universal property of $Y^X$ may be phrased thus: given any $\psi: Z \times X \to Y$, there exists a unique map $\phi: Z \to Y^X$ for which $\psi = ev_{X, Y} \circ (\phi \times 1_X)$.

Taking $Z = 1$ (the terminal object), maps $1 \to Y^X$ (or “points” of $Y^X$) are in bijection with maps $X \stackrel{\pi_{2}^{-1}}{\to} 1 \times X \to Y$. So the “underlying set” of $Y^X$, namely $\hom(1, Y^X)$, is identified with the set of maps from $X$ to $Y$. Let us denote the point corresponding to $f: X \to Y$ by $[f]: 1 \to Y^X$. Then, by definition,

$$(1 \times X \stackrel{[f] \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y) = (1 \times X \stackrel{\pi_2}{\to} X \stackrel{f}{\to} Y)$$

The following lemma says that the internal evaluation map $ev_{X, Y}$ indeed behaves as an evaluation map at the level of underlying sets.

Lemma

Given a map $f: X \to Y$ and a point $x: 1 \to X$, the composite

$$1 \stackrel{\langle [f], x \rangle}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y$$

is the point $f x: 1 \to Y$.

Proof

We have

$$\array{ 1 \stackrel{\langle [f], x \rangle}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} X & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{[f] \times x}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y\\ & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{1 \times x}{\to} 1 \times X \stackrel{[f] \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y\\ & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{1 \times x}{\to} 1 \times X \stackrel{\pi_2}{\to} X \stackrel{f}{\to} Y\\ & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{\pi_2}{\to} 1 \stackrel{x}{\to} X \stackrel{f}{\to} Y\\ & = & 1 \stackrel{x}{\to} X \stackrel{f}{\to} Y }$$

where the penultimate equation uses naturality of the projection map $\pi_2$.

Definition

Internal composition $c_{X, Y, Z}: Z^Y \times Y^X \to Z^X$ is the unique map such that

$$(Z^Y \times Y^X \times X \stackrel{c \times 1_X}{\to} Z^X \times X \stackrel{ev_{X, Z}}{\to} Z) = (Z^Y \times Y^X \times X \stackrel{1 \times ev_{X, Y}}{\to} Z^Y \times Y \stackrel{ev_{Y, Z}}{\to} Z)$$

One may show that internal composition behaves as the usual composition at the underlying set level, in that given maps $g: Y \to Z$, $f: X \to Y$, we have

$$(1 \stackrel{\langle [g], [f] \rangle}{\to} Z^Y \times Y^X \stackrel{c_{X, Y, Z}}{\to} Z^X) = [g f]: 1 \to Z^X$$

Properties

• In a cartesian closed category, the product functors $A \times -$ have right adjoints, so they preserve all colimits. In particular, a cartesian closed category that has finite coproducts is a distributive category.

• The internal logic of cartesian closed categories is minimal logic or the typed lambda-calculus.

Inheritance by reflective subcategories

In showing that a given category is cartesian closed, the following theorem is often useful (cf. A4.3.1 in the Elephant):

Theorem

If $C$ is cartesian closed, and $D\subseteq C$ is a reflective subcategory, then the reflector $L\colon C\to D$ preserves finite products if and only if $D$ is an exponential ideal (i.e. $Y\in D$ implies $Y^X\in D$ for any $X\in C$). In particular, if $L$ preserves finite products, then $D$ is cartesian closed.

Exponentials of cartesian closed categories

The following observation was taken from a post of Mike Shulman at MathOverflow.

If $\mathcal{C}$ is small and $\mathcal{D}$ is complete and cartesian closed, then $\mathcal{D}^{\mathcal{C}}$ is also complete and cartesian closed. Completeness is clear since limits in $D^C$ are computed pointwise. As for cartesian closure, we can compute exponentials in essentially the same way as for presheaves, motivated by $\mathcal{D}$-enriched category theory:

$$G^F(x) = \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} G(y)^{F(y)}.$$

Then we can compute

$$\array{ \mathcal{D}^{\mathcal{C}}\left(H,G^F\right) &=& \int_{x\in \mathcal{C}} \mathcal{D}\left(H(x), G^F(x)\right)\\ &=& \int_{x\in \mathcal{C}} \mathcal{D}\left(H(x), \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} G(y)^{F(y)}\right)\\ &=& \int_{x\in \mathcal{C}} \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} \mathcal{D}\left(H(x), G(y)^{F(y)}\right)\\ &=& \int_{y\in \mathcal{C}} \mathcal{D}\left( \int^{x\in \mathcal{C}} \sum_{\mathcal{C}(x,y)} H(x), G(y)^{F(y)}\right)\\ &=& \int_{y\in \mathcal{C}} \mathcal{D}\left(H(y), G(y)^{F(y)}\right)\\ &=& \int_{y\in \mathcal{C}} \mathcal{D}\left(H(y)\times F(y), G(y)\right)\\ &=& \mathcal{D}^{\mathcal{C}}(H\times F, G). }$$

Here the antepenultimate step uses the co-Yoneda lemma. This appears to involve colimits in $\mathcal{D}$ as well, but the existence of these colimits is not actually an extra assumption: the co-Yoneda lemma tells us that $\int^{x\in \mathcal{C}} \sum_{\mathcal{C}(x,y)} H(x)$ exists and is isomorphic to $H(y)$.

Similarly, the above argument can be interpreted to say that even if $\mathcal{D}$ is not complete, then the exponential $G^F$ in $\mathcal{D}^{\mathcal{C}}$ exists if and only if the particular limits above exist, and in that case they are isomorphic.

A more abstract argument using comonadicity and the adjoint triangle theorem, which also applies to locally cartesian closed categories, can be found in Theorem 2.12 of

• Street and Verity, The comprehensive factorization and torsors, TAC

and is reproduced in the setting of closed monoidal categories at closed monoidal category.

Functional completeness theorem

Theorem

Let $C$ be a cartesian closed category, and $c$ an object of $C$. Then the Kleisli category of the comonad $c \times - \colon C \to C$, denoted $C[c]$, is also a cartesian closed category.

Remark

The Kleisli category of the comonad $c \times -$ on $C$ is canonically equivalent to the Kleisli category of the monad $(-)^c$ on $C$.

Proof

of Theorem

Let $a$ and $b$ be objects of $C[c]$. Claim: the product $a \times b$ in $C$, considered as an object of $C[c]$, is the product of $a$ and $b$ in $C[c]$, according to the following series of natural bijections:

$$\array{ \underline{z \to a \qquad z \to b} & C[c] \\ \underline{c \times z \to a, c \times z \to b} & C \\ \underline{c \times z \to a \times b} & C \\ z \to a \times b & C[c] }$$

Claim: the exponential $a^b$ in $C$, considered as an object of $C[c]$, is the exponential of $a$ and $b$ in $C[c]$, according to the following series of natural bijections:

$$\array{ \underline{z \to a^b} & C[c] \\ \underline{c \times z \to a^b} & C \\ \underline{c \times z \times b \to a} & C \\ z \times b \to a & C[c] }$$

where in the last step, we used the prior claim that the product of objects in $C$, when viewed as an object of $C[c]$, gives the product in $C[c]$.

Observe that the object $c$ in $C[c]$ has an element $e \colon 1 \to c$, corresponding to the canonical isomorphism $c \times 1 \cong c$ in $C$. We call this element the “generic element” of $c$ in $C[c]$, according to the following theorem. This theorem can be viewed as saying that in the doctrine of cartesian closed categories, $C[c]$ is the result of freely adjoining an arrow $1\to c$ to $C$.

Theorem

(Functional completeness)

Let $C$ and $D$ be cartesian closed categories, and let $F \colon C \to D$ be a cartesian closed functor. Let $c$ be an object of $C$, and let $t: F(1) \to F(c)$ be an element in $D$. Then there exists an extension of $F$ to a cartesian closed functor $\tilde{F} \colon C[c] \to D$ that takes the generic element $e \colon 1 \to c$ in $C[c]$ to the element $t$, and this extension is unique up to isomorphism.

Proof (sketch)

On objects, $\tilde{F}(a) = F(a)$. Let $f \colon a \to b$ be a map of $C[c]$, i.e., let $g \colon c \times a \to b$ be the corresponding map in $C$, and define $\tilde{F}(f)$ to be the composite

$$F(a) \cong 1 \times F(a) \stackrel{t \times 1}{\to} F(c) \times F(a) \cong F(c \times a) \stackrel{F(g)}{\to} F(b)$$

It is straightforward to check that $\tilde{F}$ is a cartesian closed functor and is, up to isomorphism, the unique cartesian closed functor taking $e$ to $t$.

Related concepts

• exponential object, mapping space, internal hom

• convenient category of topological spaces

• cartesian closed category, locally cartesian closed category

  • cartesian doubly closed monoidal category

• cartesian closed functor, locally cartesian closed functor

• cartesian closed model category, locally cartesian closed model category

• cartesian closed 2-category

• cartesian closed (∞,1)-category, locally cartesian closed (∞,1)-category

• cartesian closed enriched category, locally cartesian closed enriched category

References

• Samuel Eilenberg, G. Max Kelly, §IV.2 of: Closed Categories, in: Proceedings of the Conference on Categorical Algebra - La Jolla 1965, Springer (1966) 421-562 [doi:10.1007/978-3-642-99902-4]

Textbook accounts:

• Saunders MacLane, §IV.6 of: Categories for the Working Mathematician, Graduate Texts in Mathematics 5 Springer (1971, second ed. 1997) [doi:10.1007/978-1-4757-4721-8]

• Francis Borceux, Def. 6.1.5 in: Categories and Structures, Vol. 2 of: Handbook of Categorical Algebra, Encyclopedia of Mathematics and its Applications 50 Cambridge University Press (1994) (doi:10.1017/CBO9780511525865)

Discussion with focus on mapping spaces (compact-open topology) in topological spaces and compactly generated topological spaces:

• Susan Niefield, Cartesianness, PhD thesis, Rutgers 1978 (proquest:302920643)

• Susan Niefield, Cartesianness: topological spaces, uniform spaces and affine schemes, J. Pure Appl. Algebra 23 (1982) 147-167 (doi:10.1016/0022-4049(82)90004-4)

See also the references at exponential object.

Establishing the syntax/semantics relation between cartesian closed categories and simply-typed lambda calculi:

• Joachim Lambek, Philip J. Scott, Part I of: Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics 7 (1986) [ISBN: 0-521-24665-2, pdf]

A proof that a cartesian closed category is posetal if it satisfies an equality of morphisms not satisfied in a free cartesian closed category:

• Kosta Dosen, and Zoran Petric. The maximality of the typed lambda calculus and of cartesian closed categories (1999), (arXiv:math/9911073)